\begin{tabbing}
$\forall$${\it es}$:ES, $a$:Atom1, $e$:E.
\\[0ex](\=(state when $e$):state@loc($e$)$>>$$a$\+
\\[0ex]$\Rightarrow$ $\neg$first($e$)
\\[0ex]$\Rightarrow$ \=loc($e$) $>>$ $a$\+
\\[0ex]$\vee$ (state when pred($e$)):state@loc(pred($e$))$>>$$a$
\\[0ex]$\vee$ isrcv(pred($e$)) \& val(pred($e$)):valtype(pred($e$))$>>$$a$)
\-\-\\[0ex]\& (\=$e$ sends $a$\+
\\[0ex]$\Rightarrow$ loc($e$) $>>$ $a$ $\vee$ (state when $e$):state@loc($e$)$>>$$a$ $\vee$ isrcv($e$) \& val($e$):valtype($e$)$>>$$a$)
\-
\end{tabbing}